/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.semantic;

import java.util.HashMap;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Set;

import salvo.jesus.graph.DirectedAcyclicGraph;
import salvo.jesus.graph.DirectedAcyclicGraphImpl;
import salvo.jesus.graph.Vertex;
import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.Module;
import alloy.ast.ModuleInfo;
import alloy.ast.Modules;
import alloy.ast.Node;
import alloy.ast.Paragraph;
import alloy.ast.Paragraphs;
import alloy.ast.QualifiedName;
import alloy.ast.SigExpr;
import alloy.ast.Signature;
import alloy.util.Dbg;
import alloy.util.Msg;
/**
 * A visitor which collects information about each
 * module in the specification for use in later semantic
 * checks.  Specifically, the visitor creates mappings from
 * names (both qualified and unqualified) to the visible paragraphs
 * in each module, and mappings from field names to all visible signatures
 * which have a field with that name (for later use in desugaring with
 * statements).
 *
 * @see ModuleScope
 */

public class MakeModuleScopesVisitor extends ASTDepthFirstVisitor
{

    /**
     * the module info for the module we are currently visiting
     */
    private ModuleInfo _curModuleInfo;
    /**
     * all the ids in the current module
     */
    private Set _curModuleIdentifiers;


    /** mapping from {@link String} qualified module names to {@link Module} modules */
    private Map _moduleNameToModule = new HashMap();


  
    /**
     * Add the relevant mappings for paragraphs which are used
     * by this module (paragraphs which can be referred to by
     * their fully qualified names).
     * @param paragraphs_ the used paragraphs
     * @see ModuleScope#addUsedParagraph(QualifiedName, Paragraph)
     */
    private void addUsedParagraphs(Paragraphs paragraphs_) {
	addUsedParagraphs(paragraphs_.getParagraphIter());
    }
    private void addUsedParagraphs(Iterator paragraphs)
    {
        // add each used paragraph to the module scope
        while(paragraphs.hasNext())
        {
            Paragraph curParagraph = (Paragraph)paragraphs.next();
            QualifiedName paraName = curParagraph.getName();
            try {
                _curModuleInfo.addUsedParagraph(paraName, curParagraph);
            } catch (AlreadyMappedException e) {
                // duplicate paragraph name
                Paragraph existingPara = null;
                try {
                    existingPara = _curModuleInfo.getParagraph(paraName);
                } catch (ModuleInfo.NoParagraphException npe) { Dbg.fatal("this can't happen"); }
        //Dbg.info("in used");
                Dbg.user(new Msg("paragraph " + existingPara.getName() + " at " + existingPara.getLocation() +
                                 " conflicts with paragraph " + curParagraph.getName(),
                                 curParagraph));
            }

        }
    }

    /**
     * Add the relevant mappings for paragraphs which are opened
     * by this module (paragraphs which can be referred to by
     * their unqualified or fully qualified names).  Note that any
     * opened paragraph is also used.
     * @param paragraphs_ the opened paragraphs
     * @see ModuleScope#addOpenedParagraph(QualifiedName, Paragraph)
     */
    private void addOpenedParagraphs(Paragraphs paragraphs_)
    {
        Iterator paragraphs = paragraphs_.getParagraphIter();
        while(paragraphs.hasNext())
        {
            Paragraph curParagraph = (Paragraph)paragraphs.next();
            QualifiedName paraName = curParagraph.getName();
            try {
                _curModuleInfo.addOpenedParagraph(paraName, curParagraph);
            } catch (AlreadyMappedException e) {
                Paragraph existingPara = null;
                try {
                    existingPara = _curModuleInfo.getParagraph(paraName);
                } catch (ModuleInfo.NoParagraphException npe) { Dbg.fatal("this can't happen"); }
        //Dbg.info("in opened");
                Dbg.user(new Msg("paragraph " + existingPara.getName().nodeString() + " at " + existingPara.getLocation() +
                                 " conflicts with paragraph " + curParagraph.getName().nodeString(),
                                 curParagraph));
            }
        }
    }
    
    private void addImportedParagraphs(Paragraphs paragraphs_) {
        Iterator paragraphs = paragraphs_.getParagraphIter();
        while(paragraphs.hasNext())
        {
            Paragraph curParagraph = (Paragraph)paragraphs.next();
            QualifiedName paraName = curParagraph.getName();
            String unqualName = paraName.getId().nodeString();
            
            // if an id with the same unqualified name as the paragraph already exists in 
            // current module, add the paragraph as used (i.e. fully qualified)
            // otherwise, add it as open (both qualified and unqualified
            try {
            	if (_curModuleIdentifiers.contains(unqualName)) {
                    _curModuleInfo.addUsedParagraph(paraName, curParagraph);
            	} else {
                    _curModuleInfo.addOpenedParagraph(paraName, curParagraph);
                } 
            } catch (AlreadyMappedException e) {
                 // duplicate paragraph name
                 Paragraph existingPara = null;
                 try {
                     existingPara = _curModuleInfo.getParagraph(paraName);
                 } catch (ModuleInfo.NoParagraphException npe) { Dbg.fatal("this can't happen"); }
            //Dbg.info("in used");
                 Dbg.user(new Msg("paragraph " + existingPara.getName() + " at " + existingPara.getLocation() +
                                  " conflicts with paragraph " + curParagraph.getName(),
                                  curParagraph));
            }
        } 	
    }

    /******** Node Methods **************/


    /**
    public void visit(Specification spec_) {
    _parent = spec_.getFocus();
    visit((Node) spec_);
    }

    **/

    /**
     * create a mapping between module names and module objects,
     * and then continue visiting tree
     * @param modules_ the set of modules
     */
    public void visit(Modules modules_)
    {
        DirectedAcyclicGraph paramDAG = new DirectedAcyclicGraphImpl();
        Map nameToVertex = new HashMap();
        
        
        for (Iterator modules = modules_.getModuleIter(); modules.hasNext();)
        {
            Module module = (Module)modules.next();
            String moduleName = module.getName().nodeString();
            Vertex v = new Vertex(module);
            nameToVertex.put(moduleName, v);
            paramDAG.add(v);
            Dbg.chk(!_moduleNameToModule.containsKey(moduleName),
                    "module " + moduleName + " appears twice in Modules");
        
            _moduleNameToModule.put(moduleName, module);
        }
        
        for (Iterator modules = modules_.getModuleIter(); modules.hasNext();) {
            Module module = (Module)modules.next();
            Vertex v1 = (Vertex)nameToVertex.get(module.getName().nodeString());
            for (Iterator params = module.getPolyParams().getQualifiedNameIter();
                 params.hasNext();){
                QualifiedName param = (QualifiedName) params.next();
                Vertex v2 = (Vertex)nameToVertex.get(param.getPath().nodeString());
                paramDAG.addEdge(v1,v2);
            }
        }
        
        for (Iterator sorted = paramDAG.reverseTopologicalSort().iterator();
             sorted.hasNext();) {
            visit((Module) ((Vertex) sorted.next()).getObject());
        }
        
    }

    private Iterator getInstantiationParagraphs(Module module_) {
	
        List sigs = new LinkedList();
	
	for (Iterator qnsIter = module_.getPolyParams().getQualifiedNameIter(); 
	     qnsIter.hasNext();) {
	    QualifiedName sigName = (QualifiedName) qnsIter.next();
	    String parentName = sigName.getPath().nodeString();
	    Module parent = (Module)_moduleNameToModule.get(parentName);
	    if (parent==null){//invalid module name 
	    		Dbg.user(new Msg(parentName+" is not a valid module name",sigName.getPath()));
	    } else {
	    		ModuleInfo parentInfo = parent.getModuleInfo();
	    		Signature sig = parentInfo.getSignature(sigName, "reference");
	    		if ((sig == null) || sig.equals(parentInfo.getUniv()) || 
	    			sig.equals(parentInfo.getInt())) continue;
	    		sigs.add(sig);
	    }
	}
   
	return sigs.iterator();
    }

    /**
     * creates a ModuleScope for a module
     * @param module_ the module
     */
    public void visit(Module module_)
    {
        _curModuleInfo = new ModuleInfo(module_);
        
        IdGatheringVisitor igv = new IdGatheringVisitor();
        module_.applyVisitor(igv);
        _curModuleIdentifiers = igv.getIds();

	
	//System.out.println("VISITING " + module_);
	//System.out.println("OPENED " + module_.getOpenedModules().nodeString());
	//System.out.println("USED " + module_.getUsedModules().nodeString());
    //System.out.println("POLYPARAMS " + module_.getPolyParams().nodeString());
	
	
        //These 4 adds are needed because there is no generic getParagraphs() method in Module
        //Add all paragraphs in current module to its scope
        addOpenedParagraphs((Paragraphs)module_.getSignatures());
        addOpenedParagraphs((Paragraphs)module_.getFacts());
        addOpenedParagraphs((Paragraphs)module_.getFunctions());
        addOpenedParagraphs((Paragraphs)module_.getPredicates());
        addOpenedParagraphs((Paragraphs)module_.getAssertions());
        // visit the signatures to get the fields
        //module_.getSignatures().applyVisitor(this);

        //Add all paragraphs in opened modules to this module's scope
        Iterator openedModuleNames = module_.getOpenedModules().getQualifiedNameIter();
        while(openedModuleNames.hasNext())
        {
            QualifiedName moduleName = (QualifiedName)openedModuleNames.next();
            String openedModuleName = moduleName.nodeString();
            Module openedModule = (Module)_moduleNameToModule.get(openedModuleName);
        //System.out.println(openedModule);
            if (openedModule == null) {
                Dbg.user(new Msg("opened non-existent module " + openedModuleName, moduleName));
                continue;
            }
//            addOpenedParagraphs((Paragraphs)openedModule.getSignatures());
//            addOpenedParagraphs((Paragraphs)openedModule.getFacts());
//            addOpenedParagraphs((Paragraphs)openedModule.getFunctions());
//            addOpenedParagraphs((Paragraphs)openedModule.getPredicates());
//            addOpenedParagraphs((Paragraphs)openedModule.getAssertions());
            
            addImportedParagraphs((Paragraphs)openedModule.getSignatures());
            addImportedParagraphs((Paragraphs)openedModule.getFacts());
            addImportedParagraphs((Paragraphs)openedModule.getFunctions());
            addImportedParagraphs((Paragraphs)openedModule.getPredicates());
            addImportedParagraphs((Paragraphs)openedModule.getAssertions());
        }

        //Add all paragraphs in used modules to this module's scope
        Iterator usedModuleNames = module_.getUsedModules().getQualifiedNameIter();
        while(usedModuleNames.hasNext())
        {
            QualifiedName moduleName = (QualifiedName)usedModuleNames.next();
            String usedModuleName = moduleName.nodeString();
        //Dbg.info(usedModuleName);
        //System.out.println("in module " + module_);
        //System.out.println("usedModuleName " + usedModuleName);
        //System.out.println(_moduleNameToModule);
        //System.out.println(_moduleNameToModule.containsKey(usedModuleName));
            Module usedModule = (Module)_moduleNameToModule.get(usedModuleName);
            if (usedModule == null) {
                Dbg.user(new Msg("used non-existent module", moduleName));
                continue;
            }
            addUsedParagraphs((Paragraphs)usedModule.getSignatures());
            addUsedParagraphs((Paragraphs)usedModule.getFacts());
            addUsedParagraphs((Paragraphs)usedModule.getFunctions());
            addUsedParagraphs((Paragraphs)usedModule.getPredicates());
            addUsedParagraphs((Paragraphs)usedModule.getAssertions());
        }

    // if module_ is a polymorphic instantiation, add the Signatures with which
    // module_ was instantiated to its visibility scope
	addUsedParagraphs(getInstantiationParagraphs(module_));

        // map the Module to its ModuleScope
        module_.setModuleInfo(_curModuleInfo);

	visit((Node) module_);
	
    }

    /** makes all SigExpr names fully qualified **/
    public void visit(SigExpr sigExpr_) {
    QualifiedName name = sigExpr_.getSig();
    if (!name.nodeString().equals("int") && name.hasEmptyPath()) {
        Signature sig = _curModuleInfo.getSignature(name,"reference");

        if (sig != null) 
	    sigExpr_.setSig(sig.getName());
    }
    }
}



















